A, B, C:MsgA. C ||decl A  C ||decl B  C ||decl A  B 

latex

Definitions	t  T, Knd, KindDeq, Id, IdDeq, P  Q, x:A. B(x), x. t(x), f || g, P & Q, Valtype(da;k), MsgA, M1 ||decl M2, mk-ma, M1  M2
Lemmas	ma-compatible-decls wf, msga wf, fpf-compatible-join, id-deq wf, Id wf, Kind-deq wf, Knd wf